Nuprl Lemma : int_iseg_properties 13,42

ij:y:{i...j}. (i  y) & (y  j
latex


Upint 1, int 1
DefinitionsTrue, T, t  T, x:AB(x), P  Q, SqStable(P), P & Q, {i...j}
Lemmasint iseg wf, decidable le, sq stable from decidable, le wf, sq stable and

origin